Nuprl Lemma : decidable__assert
9,38
postcript
pdf
b
:
. Dec(
b
)
latex
ProofTree
Definitions
t
T
,
Dec(
P
)
,
x
:
A
.
B
(
x
)
,
P
Q
,
Unit
,
,
ff
,
tt
,
,
Lemmas
bool
wf
,
btrue
wf
,
assert
wf
,
not
wf
,
assert
of
tt
,
bfalse
wf
,
assert
of
ff
origin